\chapter {La teoria degli isomorfismi}
\label{isomorfismi}

\section {Definizione di isomorfismo}
\label{sez:definizione}

\begin{definition}[tipi isomorfi] 
Diciamo che due tipi $A$ e $B$ sono isomorfi, e scriviamo $A \cong B$, se esistono due funzioni $f: A \to B$ e $g: B \to A$ tali che $f \circ g: B \to B = id_B$ e $g \circ f: A \to A = id_A$.
\label{def_iso}
\end{definition}

La definizione~\ref{def_iso} afferma che due tipi sono isomorfi nel momento in cui \`e possibile individuare una funzione $f$ che preso un valore di tipo $A$ restituisce un valore di tipo $B$ ed una funzione $g$ che preso un valore di tipo $B$ lo trasforma in un valore di tipo $A$ tali per cui la loro composizione sia l'identit\`a.\footnote{Questa non \`e l'unica definizione di isomorfismo presente in letteratura, esiste anche una definizione basata sui modelli di tipi~\cite{Deciding_1992} che si dimostra essere equivalente.}

L'intuizione che sta alla base di questa definizione \`e che se due tipi sono isomorfi sar\`a sempre possibile individuare due funzioni capaci di trasformare ogni valore del primo tipo in un valore del secondo tipo e viceversa. 
Questo tuttavia non \`e sufficiente, \`e necessario che nella conversione non vi sia nessuna perdita di informazione. \`E questa la motivazione del fatto per cui la composizione di queste due funzioni deve essere l'identit\`a.
Come sappiamo un tipo pu\`o essere visto come un insieme di valori che condividono le medesime caratteristiche, ad esempio il tipo $\tint$ rappresenta la classe di numeri interi ovvero l'insieme costituito dall'unione dei numeri naturali $\{0, 1, 2, 3, \dots\}$ e dei numeri negativi $\{-1, -2, -3, \dots\}$, il fatto che durante la conversione non debba esserci perdita di informazione significa, intuitivamente, che \`e possibile convertire un insieme pi\`u piccolo in un insieme pi\`u grande che lo contiene. Ad esempio sar\`a possibile convertire, senza perdita di informazione, l'insieme dei numeri interi nell'insieme dei numeri reali in quanto questi sono composti dai numeri interi, i numeri razionali e irrazionali.

Ad esempio, supponiamo per assurdo che si voglia dimostrare che i tipi $\tint$ e $\tbool$ siano isomorfi
\[
\tint \cong \tbool 
\]
Se questo fosse vero dovrebbe essere possibile individuare una funzione $f$ che dato un intero restituisca un booleano, come pure una funzione $g$ che preso un booleano restituisca un intero. Due funzioni che operano in questo modo potrebbero essere:
\[
\begin {array}{c}
f(n) = \vtrue \\
g(b) = 0 \\
\end {array}
\]
dove $f$ prende in input un qualunque intero $n$ e restituisce il valore $\vtrue$, mentre la funzione $g$ prende un qualsiasi valore di tipo booleano e restituisce $0$. Apparentemente queste due funzioni potrebbero essere considerate come candidate per la dimostrazione dell'isomorfismo ma in realt\`a questo non \`e possibile in quanto la loro composizione non rappresenta l'identit\`a. In particolare nella trasformazione dei tipi vi \`e una perdita di informazione, questo \`e dovuto al fatto che \textit{ogni} valore $n$ viene mappato a $\vtrue$ e \textit{ogni} valore booleano viene trasformato in $0$:
\[
\begin {array}{c}
(f \circ g)\ \vfalse = f ( g(\vtrue) ) = f (0) = \vtrue \\
(g \circ f)\ 4 = g ( f (4) ) = g (\vtrue) = 0 \\
\end {array}
\]
Da questo esempio si evince chiaramente che le due funzioni non soddisfano la definizione~\ref{def_iso}.
Si \`e quindi riusciti a dimostrare come i due tipi $\tint$ e $\tbool$ non siano isomorfi in quanto non \`e stato possibile creare una biiezione tra numeri naturali e valori booleani.

Per avere un isomorfismo \`e necessario quindi:
\begin {enumerate}
\item essere in grado di trasformare ogni valore del primo in un valore del secondo tipo,
\item di tutte le trasformazioni possibili \`e necessario considerare solo quelle che non implicano una perdita di informazione.
\end {enumerate}
Da queste considerazioni \`e chiaro il motivo per il quale i tipi:
\[
(\tint, \tunit) \cong \tint
\]
risultano essere isomorfi. Infatti, nonostante venga eliminata la componente $\tunit$ dalla coppia, questa rappresenta una componente non informativa. Esiste, infatti, un solo valore di tipo $\tunit$ la cui propriet\`a principale \`e proprio quella di avere un solo valore. Per questo le funzioni
\[
\begin {array}{c}
f (\texttt ( \textit n \texttt{, ())}) = n \\
g (n) = \texttt ( \textit n \texttt{, ())} \\
\end {array}
\]
possono essere utilizzate a dimostrazione della definizione~\ref{def_iso}.
La conversione del tipo coppia in tipo intero risulta essere banale in quanto \`e sufficiente eliminare una componente dal tipo di partenza, per effettuare l'operazione inversa \`e necessario costruire una coppia a partire da un numero intero. Sapendo che il secondo elemento deve essere di tipo $\tunit$ ed essendo questo valore unico, questa operazione risulter\`a essere estremamente semplice e non implicher\`a nessuna ambiguit\`a. Se, al contrario, si fosse dovuta costruire una coppia $(\tint, \tbool)$ a partire da un intero, la funzione $g$ non avrebbe avuto sufficienti informazioni per risolvere l'ambiguit\`a di inserire come secondo elemento il valore $\vtrue$ oppure $\vfalse$.

Per poter affermare che due tipi sono isomorfi non \`e tuttavia necessario dimostrare ogni volta la presenza di due funzioni con le caratteristiche esposte in precedenza, pi\`u avanti in questo capitolo presenteremo una tabella di isomorfismi che permetter\`a di valutare quando un tipo, anche complesso, risulta essere isomorfo ad un altro.
In particolare nella prossima sezione verr\`a introdotta la sintassi dei tipi utilizzati nel progetto, per poi passare a descrivere nella sezione~\ref{tab_iso} l'insieme delle leggi che governano gli isomorfismi e permettono, ad esempio, di eliminare tipo $\tunit$, di modificare l'associativit\`a di coppie e frecce, etc.

\section {Linguaggio di tipi}
La grammatica dei tipi di riferimento che verr\`a utilizzata per descrivere gli isomorfismi \`e la seguente:

\[
\begin{array}{rcl@{\qquad}l}
  \atype & ::= & 					& \text{\textbf{tipo}} \\
    &   & \sequence{\atype}\tref 	& \text{(predefinito)} \\
    & | & \atype \to \atype 		& \text{(funzione)} \\
    & | & \atype \times \atype 		& \text{(coppia)} \\
    & | & [ \ctor_1 : \atype_1; \dots; \ctor_n : \atype_n ] & \text{(algebrico)} \\
    & | & \tvar & \text{(variabile)} \\
    & | & \mu\tvar.\atype & \text{(ricorsivo)} \\
\end{array}
\]             

Dove la produzione $\atype ::= \sequence{\atype}\tref$ viene utilizzata per rappresentare i tipi predefiniti. Ne sono un esempio $(\alpha)\tlist$ o $(\tint)\tlist$ che rappresentano i tipi delle liste i cui elementi hanno tipo $\alpha$ oppure $\tint$. Allo stesso modo i tipi che non hanno parametri come ad esempio $\tint$, $\tfloat$ o $\tbool$ verranno rappresentati semplicemente tramite il loro nome senza parentesi.

La seconda produzione $\atype ::= \atype \to \atype$ \`e necessaria per la rappresentazione dei tipi funzione ad esempio $\atype_1 \to \atype_2$ \`e il tipo delle funzioni che hanno dominio $\atype_1$ e codominio $\atype_2$. Una funzione che prende in ingresso una lista di interi e verifica se un elemento \`e presente o meno all'interno di questa lista potrebbe essere rappresentata mediante: 
\[
(\tint) \tlist \times \tint \to \tbool
\]
dove vengono usate le coppie (pi\`u in generale le tuple) per rappresentare i parametri di una funzione.
Nella rappresentazione delle tuple verr\`a utilizzata la produzione $\atype \times \atype$ la quale permette di creare un insieme di coppie annidate della forma $\atype_1 \times (\atype_2 \times \cdots \times (\atype_{n-1} \times \atype_n)\cdots)$.

I tipi algebrici definiti anche tipi somma saranno gestiti dalla produzione $[ \ctor_1 : \atype_1; \dots; \ctor_n : \atype_n ]$ la quale permetter\`a di memorizzare, per ogni costruttore, il nome e il tipo utilizzato.
Ne sono un esempio:
\[
\textit{bool} = [\texttt{False}:\tunit; \texttt{True}:\tunit]
\]
il quale mostra il tipo che rappresenta i valori booleani o \[
\tvar \ \textit{option} = [\texttt{None}:\tunit; \texttt{Some}:\tvar]
\]
che rappresenta il tipo di un parametro il cui valore \`e opzionale.

La produzione $\atype ::= \alpha$ permette di rappresentare le variabili di tipo.

Infine \`e presente una definizione che permette di rappresentare i tipi ricorsivi, quelli cio\`e che presentano dei riferimenti a se stessi. La produzione $\atype ::= \mu\tvar.\atype$ permette infatti di rappresentare un tipo ricorsivo dove all'interno del corpo $\atype$ \`e presente un riferimento ad una variabile $\alpha$ la quale \`e definita nel tipo stesso.

Questa grammatica consente quindi di rappresentare i tipi di un qualsiasi linguaggio funzionale, supponendo ad esempio di voler descrivere il tipo di un albero informatico polimorfo otterremmo:
\[
\mu\tvar. [\texttt{Empty}:\tunit; \texttt{Node}: \beta \times (\tvar \times \tvar)]
\]
ovvero un tipo algebrico ricorsivo composto da due costruttori, il primo denominato \texttt{Empty} verr\`a utilizzato per rappresentare un albero vuoto e quindi non avr\`a nessun parametro, il secondo, \texttt{Node}, sar\`a composto dalla tupla $\beta \times (\tvar \times \tvar)$ dove gli elementi della coppia $(\tvar \times \tvar)$ rappresenteranno rispettivamente il sottoalbero sinistro e destro, mentre la variabile $\beta$ conterr\`a il valore del nodo.
Da questo esempio \`e chiaro notare come la definizione di questo albero sia polimorfa, in quanto grazie alla variabile $\beta$ \`e possibile assegnare ad un nodo qualsiasi tipo di valore.

%Durante lo sviluppo del prototipo, ci si \`e resi conto che operare con i tipi propri di OCaml risultava essere troppo complicato per riuscire ad implementare tutte le possibili sfumature degli isomorfismi. Per questo si \`e deciso di creare una struttura dei tipi intermedia (\emph{"tipi interni"}) la quale permettesse di semplificare la ricerca degli isomorfismi di tipo nelle fasi successive. Questa operazione ha anche permesso di effettuare una separazione logica tra i tipi definiti per il linguaggio di programmazione utilizzato e quelli utilizzati per il calcolo vero e proprio dell'isomorfismo. La conseguenza \`e che se si vuole utilizzare questo programma per un altro linguaggio di programmazione (pur sempre funzionale), \`e sufficiente riscrivere solo il frontend ovvero la parte che legge i tipi e li traduce in tipi interni. Il backend del programma, la parte pi\`u complessa che contiene le funzioni necessarie al calcolo degli isomorfismi e delle distanze tra i programmi, rimarr\`a la stessa.

%La tabella precedente mostra la struttura dei tipi interni i quali sono molto simili a quelli utilizzati in OCaml con l'unica differenza che i record e i tipi algebrici sono inseriti direttamente nei tipi piuttosto che essere accessibili per mezzo di riferimenti.
%L'obiettivo \`e fare in modo che i riferimenti vengano utilizzati esclusivamente per rappresentare i tipi primitivi. Nel capitolo~\ref {architettura}, verr\`a descritta in dettaglio questa fase di traduzione.

\section {Tabella degli isomorfismi}
\label{tab_iso}
Gli isomorfismi utilizzati sono esposti nella tabella~\ref{tab:eq}. Questi sono un'estensione del lavoro di Di Cosmo~\cite{Deciding_1992} nel quale \`e stata aggiunta una regola per la gestione dei tipi algebrici.
Come vedremo nel capitolo~\ref{architettura} nell'applicazione pratica di questa teoria \`e sorta la necessit\`a di gestire in modo esplicito questo tipo di costrutti.
Senza considerare questi tipi, le ricerche effettuate permettono di dimostrare~\cite{Deciding_1992} che il sistema di equazioni \`e corretto e completo rispetto al problema. 

La correttezza implica che se una equazione \`e valida allora i due tipi sono sicuramente isomorfi, la completezza \`e un concetto pi\`u sottile in quanto afferma che se due tipi sono isomorfi allora \`e possibile dimostrare per mezzo di una combinazione delle leggi appartenenti al sistema la loro equivalenza.
Nel primo caso si dimostra che applicando una regola si ottengono due tipi che sono effettivamente isomorfi, nel secondo caso, partendo dall'ipotesi che due tipi sono isomorfi, \`e necessario capire se \`e possibile definire una sequenza di applicazione ordinata di queste regole che permetta di dimostrarlo. 

Il sistema di equazioni \`e stato esteso per gestire in modo corretto i tipi algebrici, possiamo sicuramente affermare che questa regola sia corretta, ma non \`e possibile dimostrare la completezza del sistema ottenuto. Sicuramente saranno validi anche altri isomorfismi che non \`e possibile dimostrare tramite una sequenza ordinata delle regole del nostro sistema.

Ad esempio, \`e possibile definire un isomorfismo che permette di distribuire un tipo algebrico su un tipo freccia nel seguente modo:
\[
[C_1: \atype_1; C_2: \atype_2] \to \atype \cong (\atype_1 \to \atype) \times (\atype_2 \to \atype) 
\]
in quanto una funzione che possiede questo tipo si aspetta in ingresso un tipo algebrico ed \`e in grado quindi di gestire sia valori definiti mediante il costruttore $C_1$ --- che \`e di tipo $\atype_1$ --- che valori di tipo $\atype_2$ definiti tramite $C_2$ ed in entrambi i casi \`e capace di trasformarli in un valore di tipo $\atype$. Per questo una funzione definita in questo modo \`e isomorfa a due funzioni distinte che operano una su valori di tipo $\atype_1$ e una su valori di tipo $\atype_2$. \`E possibile dimostrare questa intuizione mediante le funzioni:
\begin{ScriptMath}
  $\morph$ = fun  $f$ -> ((fun $x$ -> $f$ ($C_1$ $x$)),(fun $y$ -> $f$ ($C_2$ $y$)))
  $\invmorph$ = fun ($f$, $g$) -> 
	   function 
	     $C_1$ $x$ -> $f$ $x$ 
	   | $C_2$ $y$ -> $g$ $y$
\end{ScriptMath}
ma non \`e possibile derivarlo da una applicazione delle regole esposte in tabella~\ref{tab:eq}. \`E possibile quindi affermare che, dopo l'introduzione dell'assioma per la gestione dei tipi algebrici, il sistema non gode pi\`u della propriet\`a di completezza.

Quello che \`e stato fatto \`e creare una piccola estensione del sistema assiomatico creato da Di Cosmo~\cite{Deciding_1992} che ci consenta di gestire in modo semplificato i tipi algebrici nella pratica.

Nella tabella~\ref{tab:eq} sono rappresentati tutti gli assiomi del sistema. Per ogni assioma verr\`a definita l'intuizione alla base del suo funzionamento e verranno mostrate, come nella sezione~\ref{sez:definizione}, le funzioni\footnote{Verranno mostrate le funzioni $m$ ed $\invmorph$ le quali rappresentano i morfismi, ovvero permettono di trasformare il tipo di partenza nel relativo tipo isomorfo e viceversa. In tutti i casi si osserva che se $m$ e $\invmorph$ sono i morfismi che provano la relazione $\atype_1 \eq \atype_2$ allora $\invmorph \circ m$ \`e l'identit\`a su $\atype_1$ e $m \circ \invmorph$ \`e l'identit\`a su $\atype_2$.} che permettono di dimostrare la validit\`a dell'equazione~\ref{def_iso}.

\begin{table}
\begin{center}
%\framebox{
%\parbox[\textheight]{\textwidth}{
\begin{align}
  \label{eq:pair.comm}
  \atype_1 \times \atype_2 & \eq  \atype_2 \times \atype_1
  \\
  \label{eq:pair.assoc}
  \atype_1 \times (\atype_2 \times \atype_3) & \eq  (\atype_1 \times \atype_2) \times \atype_3
  \\
  \label{eq:pair.arrow}
  (\atype_1 \times \atype_2) \to \atype_3 & \eq \atype_1 \to (\atype_2 \to \atype_3)
  \\
  \label{eq:arrow.pair}
  \atype_1 \to (\atype_2 \times \atype_3) & \eq  (\atype_1 \to \atype_2) \times (\atype_1 \to \atype_3)
  \\
  \label{eq:pair.unit}
  \atype \times \tunit & \eq  \atype
  \\
  \label{eq:arrow.unit}
  \atype \to \tunit & \eq  \tunit
  \\
  \label{eq:unit.arrow}
  \tunit \to \atype & \eq  \atype
  \\
%  \label{eq:record}
%  \{ \field_1 : \atype_1, \dots, \field_n : \atype_n \}
%  & \eq 
%  \{ \varfield_1 : \atype_1, \dots, \varfield_n : \atype_n \}
%  \\
  \label{eq:algebraic}
  {[} \ctor_1 : \atype_1; \dots; \ctor_n : \atype_n {]}
  & \eq 
  [ \varctor_{\sigma(i)} : \atype_1; \dots; \varctor_{\sigma(n)} : \atype_n ]
  \\
  \label{eq:forall.perm}
  \forall \tvar.\forall \vartvar.\atype & \eq  \forall \vartvar.\forall \tvar.\atype
  \\
  \label{eq:forall.rename}
  \forall \tvar.\atype & \eq  \forall \vartvar.\atype\subst{\vartvar}{\tvar}
  & \vartvar \not\in \fv(\atype)
  \\
  \label{eq:rec.rename}
  \mu\tvar.\atype & \eq  \mu\vartvar.\atype\subst{\vartvar}{\tvar}
  & \vartvar \not\in \fv(\atype)
  \\
  \label{eq:split}
  \forall \tvar.(\atype_1 \times \atype_2) & \eq  \forall \tvar.\forall \vartvar.(\atype_1 \times \atype_2\subst{\vartvar}{\tvar})
  \\
  \label{eq:forall.unit}
  \forall \tvar.\atype & \eq  \tunit
  & \atype \eq \tunit 
\end{align}
%}
%}
\end{center}
\caption{\label{tab:eq} Isomorfismi tra tipi di riferimento}
\end{table}

%\begin{ScriptMath}
%  let id = fun $x$ -> $x$
%  let fst = fun ($x$, _) -> $x$
%  let snd = fun (_, $x$) -> $x$
%  let ($\circ$) = fun $f$ $g$ -> fun $x$ -> $f$ ($g$ $x$)
%\end{ScriptMath}

%\begin{enumerate}
\paragraph{\ref{eq:pair.comm} Commutativit\`a delle coppie:} l'ordine nella disposizione degli elementi di una coppia non \`e rilevante ai fini della semantica di un tipo. Com'\`e facile intuire, infatti, scambiando l'ordine di due elementi appartenenti ad una coppia non vi \`e nessuna perdita di informazione sul tipo. Le due funzioni che permettono di dimostrare questo assioma sono:
\begin{ScriptMath}
  $\morph$ = fun ($x$, $y$) -> ($y$, $x$)
  $\invmorph$ = $\morph$
\end{ScriptMath}
Se si considera l'esempio esposto in precedenza degli alberi informatici polimorfi si capisce come non sia significativa la posizione del valore del nodo rispetto ai due sotto alberi, \`e possibile pertanto affermare che:
\[
\texttt{Node}: \beta \times (\tvar \times \tvar) \cong \texttt{Node}: (\tvar \times \tvar) \times \beta
\]

\paragraph{\ref{eq:pair.assoc} Associativit\`a delle coppie:} come diretta conseguenza dell'assioma precedente e della struttura della produzione che permette di creare una tupla, anche in questo caso modificando l'ordine di applicazione delle coppie non vi \`e alcuna perdita di informazione, \`e possibile dimostrare l'isomorfismo mediante:
\begin{ScriptMath}
  $\morph$ = fun ($x$, ($y$, $z$)) -> (($x$, $y$), $z$)
  $\invmorph$ = fun (($x$, $y$), $z$) -> ($x$, ($y$, $z$))
\end{ScriptMath}
Riprendendo l'esempio precedente e applicando le prime due leggi di isomorfismo \`e possibile rappresentare un nodo, isomorfo quello di partenza, in questo modo:
\[
\texttt{Node}: \beta \times (\tvar \times \tvar) \cong \texttt{Node}: \tvar \times (\beta \times \tvar)
\]
ovvero come una tupla composta dal sotto l'albero di sinistra, il valore del nodo e il sotto albero destro.

\paragraph{\ref{eq:pair.arrow} Currying:} nei linguaggi di programmazione funzionali le funzioni a pi\`u argomenti non hanno ragione di esistere dal momento in cui \`e possibile definire delle funzioni che prendono in ingresso o restituiscono altre funzioni. Questa caratteristica, denominata \textit{currying}, permette di fatto di rendere isomorfe le funzioni $(\atype_2 \times \atype_2) \to \atype_3 $ e $\atype_1 \to (\atype_2 \to \atype_3)$.

La dimostrazione dell'isomorfismo deriva da:
\begin{ScriptMath}
  $\morph$ = fun $f$ -> fun $x$ $y$ -> $f$ ($x$, $y$)
  $\invmorph$ = fun $f$ -> fun ($x$, $y$) -> $f$ $x$ $y$
\end{ScriptMath}

Ad esempio la funzione descritta precedentemente che prende una coppia composta da una lista di interi, un valore di tipo intero e restituisce un valore booleano che rappresenta la presenza o meno di quel valore all'interno della lista potrebbe essere:
\begin{ScriptMath}
fun ($l$,$n$) -> $E$ 
\end{ScriptMath}
dove $E$ rappresenta il corpo della funzione la cui struttura non \`e rilevante ai fini del discorso, il cui tipo \`e:
\[
((\tint)\tlist \times \tint) \to \tbool 
\]
la quale risulta isomorfa alla versione ``currificata'' della somma definita in questo modo:
\begin{ScriptMath}
fun $l$ -> fun $n$ -> $E$
\end{ScriptMath}
che ha tipo:
\[
(\tint)\tlist \to (\tint \to \tbool) 
\]

\paragraph{\ref{eq:arrow.pair} Distributivit\`a delle funzioni sulle coppie:} \`e possibile dimostrare la propriet\`a distributiva del tipo freccia sul tipo coppia nel seguente modo:
\begin{ScriptMath}
  $\morph$ = fun $f$ -> (fst $\circ$ $f$, snd $\circ$ $f$)
  $\invmorph$ = fun ($f$, $g$) -> fun $x$ -> ($f$ $x$, $g$ $x$)
\end{ScriptMath}
\textit{dove:}
\begin{ScriptMath}
  let fst = fun ($x$, _) -> $x$
  let snd = fun (_, $x$) -> $x$
  let ($\circ$) = fun $f$ $g$ -> fun $x$ -> $f$ ($g$ $x$)
\end{ScriptMath}

\paragraph{\ref{eq:pair.unit} Il tipo $\tunit$ \`e superfluo:} il tipo $\tunit$ all'interno di una coppia non apporta nessuna informazione, la motivazione di questo fatto \`e stata descritta nella sezione~\ref{sez:definizione}. Tramite la funzione \textit{fst} che restituisce il primo elemento di una coppia \`e possibile definire i morfismi nel seguente modo:
\begin{ScriptMath}
  $\morph$ = fst
  $\invmorph$ = fun $x$ -> ($x$, ())
\end{ScriptMath}

\paragraph{\ref{eq:arrow.unit} Un linguaggio funzionale puro non ha effetti collaterali:} questa regola \`e valida solo per i linguaggi funzionali puri, ovvero quelli in cui non si hanno side-effect. Le due funzioni che permettono di dimostrare questo isomorfismo sono:
\begin{ScriptMath}
  $\morph$ = fun _ -> ()
  $\invmorph$ = fun () -> fun _ -> ()
\end{ScriptMath}
Nei linguaggi impuri, al contrario, la gestione della memoria e la stampa a video sono gestite in modo esplicito, quindi questo isomorfismo non \`e applicabile.

\paragraph{\ref{eq:unit.arrow} Funzione con parametro $\tunit$:} se una funzione ha un unico parametro e questo \`e $\tunit$, \`e possibile considerarla isomorfa ad il solo tipo che questa restituisce. Intuitivamente una funzione definita in questo modo non prende in ingresso alcun valore e restituisce un risultato di un determinato tipo. Si pu\`o affermare pertanto che questa non dipenda da nessun dato proveniente dall'esterno, l'unica informazione significativa \`e il tipo di dato che questa restituisce. Anche questa regola come la precedente, \`e valida esclusivamente per linguaggi di programmazione funzionali puri. Supponendo infatti di avere una funzione definita nel seguente modo:
\begin{ScriptMath}
fun () -> $\tint$ 
\end{ScriptMath}
non \`e sempre corretto considerarla isomorfa ad il solo tipo intero in quanto se il linguaggio di programmazione \`e impuro questa potrebbe essere rappresentativa di una funzione che prende in ingresso un valore da tastiera e che ogni volta che viene applicata a $\tunit$ restituisce un risultato diverso. Considerarla isomorfa ad il solo tipo $\tint$ significa considerarla equivalente ad un valore costante. 

Nel caso di linguaggi funzionali puri il morfismo che permette di dimostrare questo assioma \`e:
\begin{ScriptMath}
  $\morph$ = fun $f$ -> $f$ ()
  $\invmorph$ = fun $x$ -> fun () -> $x$
\end{ScriptMath}

%\paragraph{\ref{eq:record} Il nome dei campi di un record \`e irrilevante:} questa regola \`e stata inserita nel sistema di equazioni per poter dichiarare come isomorfi due record i quali contengono gli stessi campi ma ordinati in modo differente. Il morfismo che permette di dimostrarlo \`e:
%\begin{ScriptMath}
%  $\morph$ = fun { $f_1$ = $x_1$, $\dots$, $f_n$ = $x_n$ } -> { $g_1$ = $x_1$, $\dots$, $g_n$ = $x_n$ }
%  $\invmorph$ = fun { $g_1$ = $x_1$, $\dots$, $g_n$ = $x_n$ } -> { $f_1$ = $x_1$, $\dots$, $f_n$ = $x_n$ }
%\end{ScriptMath}

\paragraph{\ref{eq:algebraic} Nome e ordine dei costruttori di un tipo algebrico sono irrilevanti:} questa regola \`e stata introdotta ad-hoc nel sistema di equazioni per poter enfatizzare il fatto che, in un tipo algebrico, l'unica informazione importante \`e il \emph{tipo} dei costruttori. 
Per definire questa situazione \`e necessario riuscire a creare una biiezione sulle componenti del tipo algebrico ($\sigma$ \`e una biiezione su $\{1,\dots,n\}$ in~\ref{tab:eq}):
\begin{ScriptMath}
  $\morph$ = function
            $\ctor_1$ $x_1$ -> $\varctor_{\sigma(1)}$ $x_1$
              $\vdots$
          | $\ctor_n$ $x_n$ -> $\varctor_{\sigma(n)}$ $x_n$
  $\invmorph$ = function
            $\varctor_{\sigma(1)}$ $x_1$ -> $\ctor_1$ $x_1$
              $\vdots$
          | $\varctor_{\sigma(n)}$ $x_n$ -> $\ctor_n$ $x_n$
\end{ScriptMath}
Ad esempio, nel caso dell'albero descritto in precedenza il nome che si decide di assegnare ai costruttori \`e irrilevante, non vi \`e motivo infatti di distinguere i due tipi:
\[
\mu\tvar. [\texttt{Empty}:\tunit; \texttt{Node}: \beta \times (\tvar \times \tvar)] \cong \mu\tvar. [\texttt{Vuoto}:\tunit; \texttt{Nodo}: \beta \times (\tvar \times \tvar)]
\]

\paragraph{\ref{eq:forall.perm} L'ordine di quantificazione dei parametri di un tipo polimorfo \`e irrilevante:} la funzione che permette di dimostrare l'isomorfismo sotto queste condizioni \`e:
\begin{ScriptMath}
  $\morph$ = id
  $\invmorph$ = id
\end{ScriptMath}
\textit{dove:}
\begin{ScriptMath}
  let id = fun $x$ -> $x$
\end{ScriptMath}

\paragraph{\ref{eq:forall.rename} Il nome dei parametri di un tipo polimorfo \`e irrilevante:} quando viene definita una variabile di tipo non \`e importante il nome che viene assegnato ad essa. Una variabile di tipo non \`e altro che un modo per rappresentare un oggetto che pu\`o contenere qualunque tipo al suo interno. Per questo assegnare ad una variabile un nome piuttosto che un altro non modifica le informazioni che questa porta con s\'e.
La funzione identit\`a \`e un chiaro esempio che permette di mostrare l'isomorfismo:
\begin{ScriptMath}
  $\morph$ = id
  $\invmorph$ = id
\end{ScriptMath}
Nell'esempio precedente del nodo dell'albero polimorfo non \`e rilevante il nome delle variabili di tipo, pertanto:
\[
\texttt{Node}: \beta \times (\tvar \times \tvar)] \cong \texttt{Node}: \gamma \times (\tvar \times \tvar)]
\]
risultano essere isomorfi.

\paragraph{\ref{eq:rec.rename} Il nome di un tipo ricorsivo \`e irrilevante:} definire un tipo ricorsivo significa che all'interno di questo vengono effettuati dei riferimenti a se stesso, \`e chiaro quindi come il nome che si assegna non sia significativo le funzioni che permettono di dimostrarlo sono:
\begin{ScriptMath}
  $\morph$ = id
  $\invmorph$ = id
\end{ScriptMath}
Ad esempio la definizione del tipo ricorsivo albero polimorfo:
\[
\mu\tvar. [\texttt{Empty}:\tunit; \texttt{Node}: \beta \times (\tvar \times \tvar)]
\]
\`e equivalente al tipo in cui $\tvar$ viene ridenominata in $\gamma$  :
\[
\mu\gamma. [\texttt{Empty}:\tunit; \texttt{Node}: \beta \times (\gamma \times \gamma)]
\]
naturalmente \`e necessario prestare attenzione al fatto che nella ridenominazione la nuova variabile non debba occorrere come variabile libera.\footnote{Una variabile si definisce libera quando non \`e legata da nessun quantificatore, nell'esempio la variabile $\tvar$ \`e legata dal quantificatore $\forall$} Si sarebbero infatti creati dei conflitti se si fosse deciso di rinominare $\tvar$ in $\beta$ ottenendo:
\[
\mu\beta. [\texttt{Empty}:\tunit; \texttt{Node}: \beta \times (\beta \times \beta)]
\]
che non risulta essere isomorfo al tipo di partenza.

\paragraph{\ref{eq:split} I parametri nelle componenti di una coppia polimorfa sono indipendenti:} nel caso in cui una coppia sia composta da tipi polimorfi che condividono la stessa variabile di tipo, \`e possibile avere la certezza che sostituendo ad un solo elemento della coppia una variabile con una nuova, il tipo ottenuto \`e isomorfo a quello di partenza. Questo significa che all'interno di una coppia non vi \`e nessuna condivisione delle variabili di tipo ovvero che non vi \`e ragione di distinguere i tipi:
\[
(\tvar \times \tvar) \cong (\tvar \times \tvar_1) 
\]
quest'assioma deriva dal fatto che, come esposto precedentemente, una variabile di tipo non \`e altro che un modo astratto per rappresentare un qualunque tipo di valore, pertanto all'interno di una coppia rinominare una componente non modifica la semantica del tipo, la dimostrazione \`e data da:

\begin{ScriptMath}
  $\morph$ = id
  $\invmorph$ = fun $x$ -> (fst $x$, snd $y$)
\end{ScriptMath}

\paragraph{\ref{eq:forall.unit} Il polimorfismo del tipo $\tunit$ \`e irrilevante:} questa regola \`e una chiara conseguenza del fatto che il tipo $\tunit$ non porta con s\'e nessuna informazione, in questo caso $\morph$ ed $\invmorph$ coincidono con i morfismi che provano che $\atype \cong \tunit$

\section {Algoritmo}
Nelle discipline informatiche, come in quelle matematiche, quando si pone il problema di realizzare un processo che si basa su un sistema assiomatico, \`e una pratica comune trasformare il dato in ingresso in una forma sintatticamente differente che permetta di semplificare la fase finale di applicazione delle equazioni.
%Ad esempio, nella logica matematica, la trasformazione in forma normale congiuntiva o disgiuntiva delle formule \`e un chiaro esempio di normalizzazione che permette di ottenere una forma sintattica della formula che permette di rendere il problema della soddisfacibilit\`a estremamente semplice.

In queste fasi intermedie si cerca sempre di approssimare il modello rappresentato dal sistema assiomatico. Se si immagina questo modello come un albero informatico le fasi di normalizzazione hanno come obiettivo la ristrutturazione della struttura del dato in ingresso con lo scopo di renderla quanto pi\`u simile a questo albero.

Nel caso specifico del nostro progetto \`e stato necessario individuare una tecnica che permettesse di riscrivere il tipo di partenza in una forma simile al modello del sistema assiomatico per la verifica degli isomorfismi esposto nella tabella~\ref{tab:eq}.
Questa trasformazione \`e avvenuta in due fasi successive:
\begin{itemize}
\item trasformazione in forma normale (n.f.(A));
\item trasformazione in forma normale split (s.n.f.(A)).
\end{itemize}
Ottenuto il secondo tipo di forma normale la verifica dell'isomorfismo si \`e ridotta ad un semplice confronto sintattico tra i tipi.

Nei prossimi paragrafi verranno descritte le tecniche utilizzate per le trasformazioni in forme normali, infine verr\`a descritto il metodo di confronto utilizzato per verificare gli isomorfismi.

\subsection{Trasformazione in forma normale}
La trasformazione in forma normale ha come obiettivo la trasformazione del tipo originario per renderlo sintatticamente pi\`u simile al modello assiomatico degli isomorfismi esposto nella tabella~\ref{tab:eq}.
Per fare questo si \`e partiti proprio da un sottoinsieme di questi assiomi i quali sono stati trasformati in regole di riscrittura, ovvero ne \`e stata definita una direzione univoca di applicazione.\footnote{Questa tecnica \`e comunemente denominata \emph{narrowing}.}
Quello che si \`e ottenuto \`e esposto nella tabella~\ref{tab:rew}.
\begin{table}
\begin{center}
%\framebox{
%\parbox[\textheight]{\textwidth}{
\begin{align}
  \label{narr:pair.assoc}
  \atype_1 \times (\atype_2 \times \atype_3) & \leadsto  (\atype_1 \times \atype_2) \times \atype_3
  \\
  \label{narr:pair.arrow}
  (\atype_1 \times \atype_2) \to \atype_3 & \leadsto \atype_1 \to (\atype_2 \to \atype_3)
  \\
  \label{narr:arrow.pair}
  \atype_1 \to (\atype_2 \times \atype_3) & \leadsto  (\atype_1 \to \atype_2) \times (\atype_1 \to \atype_3)
  \\
  \label{narr:pair.unit}
  \atype \times \tunit & \leadsto  \atype
  \\
  \label{narr:pair.unit2}
  \tunit \times \atype & \leadsto  \atype
  \\
  \label{narr:arrow.unit}
  \atype \to \tunit & \leadsto  \tunit
  \\
  \label{narr:unit.arrow}
  \tunit \to \atype & \leadsto  \atype
  \\
  \label{narr:forall.unit}
  \forall \tvar.\atype & \leadsto  \tunit
  & \atype \eq \tunit 
\end{align}
%}
%}
\end{center}
\caption{\label{tab:rew} Riscrittura dei tipi \OCaml.}
\end{table}
Come si pu\`o intuire a questo punto il sistema di riscrittura ha permesso, mediante l'applicazione successiva delle regole esposte nella tabella, di ottenere un tipo semanticamente equivalente (isomorfo) a quello di partenza ma con una sintassi differente.

\`E stato dimostrato~\cite{Deciding_1992}, che il sistema di riscrittura in tabella~\ref{tab:rew} \`e un sistema \textit{normalizzante} e \textit{confluente}. 
La prima caratteristica consente di ottenere, dopo un numero finito di trasformazioni, una forma nella quale non \`e possibile applicare ulteriori regole (\emph{forma normale}). 
La caratteristica di confluenza permette invece di avere la certezza che il risultato ottenuto sia indipendente dall'ordine con cui le regole vengono applicate. \`E possibile infatti che per un tipo sia possibile applicare pi\`u forme di riscrittura, se il sistema \`e confluente l'ordine con cui si applicano tali trasformazioni \`e irrilevante.
Ad esempio, suppenendo che si voglia dimostrare l'isomorfismo tra i tipi:
\[
(\tint \to \tbool \to \tint) \times (\tunit \times \tstring) \cong \tstring \to (\tunit \times \tint \to \tint)
\]
la trasformazione in forma normale del primo tipo sarebbe:
\[
\begin{array}{rrl}
\multicolumn{3}{l}{(\tint \to \tbool \to \tint) \times (\tunit \times \tstring) } \\ 
\hspace{4cm} & \leadsto & ((\tint \to \tbool \to \tint) \times \tunit) \times \tstring
\\ 
& \leadsto & (\tint \to \tbool \to \tint) \times \tstring \\
\end{array}
\]
dove l'applicazione in sequenza delle regole~\ref{narr:pair.assoc} e~\ref{narr:pair.unit} porta ad un risultato nel quale non \`e pi\`u possibile applicare ulteriori forme di riscrittura (propriet\`a normalizzante). 
Per il secondo tipo l'applicazione di~\ref{narr:arrow.pair} e di~\ref{narr:arrow.unit} permette di arrivare alla forma normale:
\[
\begin{array}{rcl}
\multicolumn {3}{l}{\tstring \to (\tunit \times \tint \to \tint)} \\ 
\hspace{3cm} & \leadsto & (\tstring \to \tunit) \times (\tstring \to \tint \to \tint) \\
& \leadsto & \tstring \times (\tstring \to \tint \to \tint) \\
\end{array}
\]
\`E da notare come il risultato sarebbe stato lo stesso se avessimo utilizzato la regola~\ref{narr:pair.unit2} sul secondo elemento del tipo freccia (propriet\`a di confluenza).

%La correttezza di questo processo risiede nella caratteristica di completezza del sistema. Abbiamo gi\`a definito questa idea come la capacit\`a di identificare un ordine di applicazione delle equazioni che permetta di dimostrare che un determinato tipo, anche complesso, sia isomorfo ad un altro. Come sappiamo al nostro sistema di equazioni sono stati aggiunti degli assiomi per la gestione dei record e dei tipi algebrici, i quali per\`o non sono sufficienti a dimostrare tutti gli isomorfismi possibili. 

Alla fine di questa prima fase di riscrittura il tipo ottenuto avr\`a la forma
\[
	\forall X.(A_1 \times A_2 \times \cdots \times A_n)
\]
dove \`e presente una tupla della forma $(A_1 \times A_2 \times \cdots \times A_n)$ la quale \`e composta da una serie di coordinate $A_i$ all'interno delle quali non compaiono coppie o il tipo $\tunit$.

Nell'esempio precedente le coordinate sono:
\[
\begin{array}{c}
(\tint \to \tbool \to \tint) \times \tstring \equiv A_1 \times A_2 \\
\tstring \times (\tbool \to \tint \to \tint) 
\equiv B_1 \times B_2 
\end{array}
\] 

\subsection{Trasformazione in forma normale split}
Da ricerche condotte da Di Cosmo~\cite{Deciding_1992} \`e risultato che per semplificare ulteriormente la fase decisionale finale, \`e necessario introdurre un'ulteriore forma normale che si basa sull'assioma \emph{split} (equazione~\ref{eq:split} della tabella~\ref{tab:eq}).
L'idea \`e quella di ottenere un tipo nella forma:
\[
	\forall X_1, X_2, \dots, X_n (A_1 \times A_2 \times \dots \times A_n).
\]
che \`e molto simile al precedente ma nel quale le coordinate $A_i$ non condividono nessuna variabile di tipo. 
In altre parole questa regola afferma che, in base alla regola \emph{split}, effettuando una ridenominazione \`e sempre possibile ricondursi ad un tipo in cui coordinate diverse non condividono mai la stessa variabile.
Si prenda come esempio il tipo:
\[
\forall \alpha.(\alpha \to \alpha) \times (\alpha \to \alpha) 
\]
questo \`e in forma normale ma non in forma normale split in quanto sono presenti due coordinate $A_1 = (\alpha \to \alpha)$ e $A_2 = (\alpha \to \alpha)$ che condividono la stessa variabile $\alpha$.
Naturalmente \`e importante precisare che dopo questo passaggio la forma normale non \`e pi\`u unica. Questa infatti dipender\`a dal nome --- arbitrario --- con il quale si decide di rinominare le variabili. Verr\`a meno quindi la propriet\`a normalizzante che caratterizzava il sistema di riscrittura precedente.

\subsection{Confronto tra tipi}
Ottenuta la forma canonica split del tipo originario, \`e possibile procedere con la fase di confronto dei tipi. 
Per effettuare questa operazione \`e necessario individuare un ordine di applicazione degli assiomi esposti in tabella~\ref{tab:eq}, che permetta di identificare un isomorfismo.
Il problema principale \`e che questo potrebbe causare una perdita del potere espressivo del sistema, ad esempio se si decide di applicare in sequenza le seguenti leggi del sistema assiomatico~\ref{tab:eq}:
\begin{enumerate}
\item commutativit\`a del prodotto
\item regola swap
\item swap sui quantificatori
\item restanti assiomi
\end{enumerate}
una volta applicata la commutativit\`a del prodotto, la regola swap, e lo swap sui quantificatori, non \`e possibile applicare nuovamente la legge sulla commutativit\`a. In questo modo cio\`e si definiscono una serie di operazioni che \`e necessario eseguire in modo sequenziale l'una dopo l'altra, rispetto ad un sistema assiomatico il quale definisce un insieme di leggi delle quali non \`e specificato un ordine di applicazione definito.

Dalle ricerche effettuate da Di Cosmo~\cite{Deciding_1992}, \`e risultato che applicando in sequenza le leggi come descritto in precedenza, non vi \`e alcuna perdita del potere espressivo del sistema.
Si \`e quindi implicitamente definito l'algoritmo per la verifica degli isomorfismi, il quale operer\`a nel seguente modo:
\begin{enumerate}
\item Fase 1: Commutativit\`a del prodotto di coordinate 
\item Fase 2: Applicazione della regola swap all'interno delle coordinate
\item Fase 3: Applicazione della regola swap sulle variabili di tipo.
\end{enumerate}
Verr\`a cio\`e effettuata una prima fase dove verranno definiti isomorfi due tipi nei quali \`e stato scambiato l'ordine delle coordinate, successivamente verr\`a verificato quando due di queste sono isomorfe in base alla regola swap, infine il sistema sar\`a reso insensibile ad eventuali modifiche sul nome delle variabili di tipo mediante l'applicazione della regola swap sui quantificatori.

Nelle prossime sezioni verranno descritte dettagliatamente queste fasi.

%Il passo successivo alla trasformazione in forma canonica split del tipo originario, \`e l'individuazione di un ordine di applicazione degli assiomi in tabella~\ref{tab:eq} che permetta di identificare un algoritmo per il confronto tra tipi.
%Da ricerche effettuate~\cite{Deciding_1992} \`e risultato che applicando in sequenza:
%\begin{enumerate}
%\item commutativit\`a del prodotto
%\item regola swap
%\item swap sui quantificatori
%\item restanti assiomi
%\end{enumerate}
%non vi \`e alcuna perdita del potere espressivo del sistema assiomatico ed essendo riusciti a definire una sequenza di operazioni implicitamente \`e stato definito un algoritmo per il calcolo degli isomorfismi.

\subsubsection{Fase 1: commutativit\`a delle coordinate}
La prima fase del confronto si basa sul fatto che, dopo la conversione in forma normale split, si ottiene un tipo nella forma:
\[ 
	A_1 \times A_2 \times \dots \times A_n 
\]
ovvero una tupla composta da $n$ elementi (che indicheremo con il nome di coordinate) all'interno dei quali non possono comparire ulteriori prodotti o il tipo $\tunit$. Data la particolare struttura di questa forma normale, risulta estremamente semplice astrarre dall'ordine delle componenti della tupla.
Se rappresentiamo, infatti, le coordinate come elementi di una lista:\footnote{In questi esempi il simbolo $\Longrightarrow$ \`e utilizzato per indicare il modo in cui vengono rappresentati i tipi nell'algoritmo. Ad esempio $[X_1, X_2, \dots, X_n]$ rappresenta una lista composta dai valori $X_1, X_2, \dots, X_n$}

\[
	A_1 \times A_2 \times \dots \times A_n \Longrightarrow [A_1;A_2;\dots;A_n] 
\]
sar\`a sufficiente verificare che:
\begin {itemize}
\item le liste abbiano lo stesso numero di valori;
\item esista una permutazione degli elementi della prima lista tale per cui ogni elemento \`e isomorfo al corrispondente della seconda lista.
\end{itemize}
Nel caso in cui le liste abbiano lunghezza differente, non vi \`e nessuna possibilit\`a che i due tipi siano isomorfi, in quanto durante la fase di normalizzazione sono state eliminate tutte le componenti $\tunit$ le quali permetterebbero di avere due tipi isomorfi ma con un numero di coordinate differente. In caso contrario sar\`a necessario individuare, per ogni elemento della prima lista, un elemento della seconda che sia \emph{isomorfo} al primo.

Ad esempio, nella sezione precedente si \`e arrivati ad ottenere i due tipi in forma normale:
\[
\begin{array}{c}
(\tint \to \tbool \to \tint) \times \tstring \Longrightarrow [A_1; A_2] \\
\tstring \times (\tbool \to \tint \to \tint) 
\Longrightarrow [B_1; B_2] \\
\end{array}
\] 
che verranno rappresentati mediante due liste di due elementi. A questo punto \`e necessario individuare una permutazione degli elementi della prima lista che permetta di rendere ogni componente isomorfo al corrispondente della seconda lista:
\[
\begin{array}{c}
(\tint \to \tbool \to \tint) \times \tstring \Longrightarrow [A_1; A_2] \\
(\tbool \to \tint \to \tint) \times \tstring  
\Longrightarrow [B_2; B_1] \\
\end{array}
\]

\subsubsection {Fase 2: permutazione degli argomenti nelle coordinate}
La verifica dell'isomorfismo tra due coordinate risulta essere banale nel caso di tipi atomici (i tipi $\tstring$ delle coordinate $A_2$ e $B_1$ sono chiaramente equivalenti), quando questi sono complessi, come nel caso di $A_1$ e $B_2$ \`e necessario definire un metodo per individuare l'isomorfismo. 

Ecco allora la necessit\`a della seconda fase del confronto la quale opera pi\`u in profondit\`a all'interno delle coordinate. 
Com'\`e stato precedentemente illustrato, in ogni coordinata saranno presenti esclusivamente tipi freccia e tipi atomici. Sotto queste condizioni l'assioma swap permette di considerare come isomorfi due tipi freccia che condividono il codominio ma che hanno subito la permutazione degli argomenti. 
Per verificare swap il tipo verr\`a rappresentato mediante una coppia composta di due elementi:
\begin{itemize}
\item una lista contenente tutti gli argomenti della funzione,
\item un elemento che rappresenta il codominio.
\end{itemize}
In questo modo: 
\[
	A_1: X_1 \to X_2 \to \dots \to X_{n-1} \to X_n \Longrightarrow ([X_1, X_2,\dots, X_{n-1}], X_n)
\] 
A questo punto verificare se due tipi sono isomorfi risulta essere estremamente semplice in quanto sar\`a sufficiente verificare che:
\begin{itemize}
\item il numero degli elementi $X_1,\dots,X_{n-1}$ delle liste sia uguale,
\item gli elementi delle liste siano isomorfi a coppie (come gi\`a esposto per le coordinate),
\item il secondo elemento della coppia, il codominio, sia equivalente.
\end{itemize}
Nell'esempio precedente le coordinate da verificare sono $A_1$ e $B_2$ ovvero:
\[
\begin{array}{c}
A_1: \tint \to \tbool \to \tint \\
B_2: \tbool \to \tint \to \tint \\
\end{array}
\]
le quali verranno rappresentate nel seguente modo:
\[
\begin{array}{c}
A_1: ([\tint, \tbool], \tint) \\
B_2: ([\tbool, \tint], \tint) \\
\end{array}
\]
come si pu\`o notare i codomini risultano essere equivalenti ed \`e possibile, per ogni elemento della prima lista, individuarne un corrispondente della seconda che risulta essere isomorfo al primo. Sotto queste condizioni possiamo quindi affermare che le due coordinate $A_1$ e $B_2$ sono isomorfe.
Questo esempio risulta essere estremamente semplice, \`e possibile infatti che siano essere necessarie ulteriori ricorsioni sulla seconda fase dell'algoritmo che permettano di entrare ancora pi\`u in profondit\`a all'interno delle coordinate.

La prima fase del confronto ha operato sulle coppie, la trasformazione in forma normale, infatti, ha permesso di rappresentare il tipo di partenza mediante coppie di coordinate. \`E stato possibile a questo livello ignorare l'ordine degli elementi ed applicare quindi la propriet\`a commutativa esposta nella tabella~\ref{tab:eq}. 
A questo punto \`e stato necessario introdurre un'ulteriore fase che permettesse di verificare quando due elementi (coordinate) risultassero isomorfi. Si \`e passati quindi ad un livello pi\`u basso nel quale l'applicazione dell'assioma swap ha permesso di essere insensibili ad eventuali permutazioni negli argomenti di una funzione.

\subsubsection {Fase 3: variabili di tipo}
In tutti questi passaggi sono state volontariamente tralasciate le variabili di tipo. 
La terza fase del confronto si occupa appunto della corretta gestione di questi elementi, facendo in modo che il nome\footnote{Come sappiamo, infatti, il nome della variabile di tipo \`e solo una astrazione che permette di rappresentare un qualunque tipo.} che viene assegnato ad una determinata variabile all'interno di un tipo non sia significativo nella ricerca degli isomorfismi.

Si desidera, ad esempio, fare in modo che i due tipi:
\[
	\forall \alpha, \beta. \alpha \to \beta \to \tint \cong \forall \gamma, \delta. \gamma \to \delta \to \tint 
\]
siano considerati isomorfi.

In linea teorica dagli studi effettuati da Di Cosmo~\cite{Deciding_1992} \`e risultato che per effettuare questa operazione \`e necessario verificare l'esistenza di una permutazione delle variabili che compaiono nel primo tipo tale per cui dopo una riscrittura di queste variabili \`e possibile ottenere il secondo tipo.
Ovvero \`e necessario individuare una tecnica che permetta di rinominare le variabili (utilizzando quelle del secondo tipo) in modo da identificare un isomorfismo.
Ad esempio, rinominando $\alpha$ in $\gamma$ e $\beta$ in $\delta$, nell'esempio precedente si ottiene: 
\[
	\forall \gamma, \delta. \gamma \to \delta \to \tint \cong \forall \gamma, \delta. \gamma \to \delta \to \tint 
\]
i quali risultano essere equivalenti.
Anche in questo caso, come nelle precedenti fasi, nel momento in cui si individua che il numero di variabili \`e diverso nei due tipi, non vi \`e alcuna speranza che questi possano essere isomorfi.
Questa fase risulta essere estremamente importante in quanto le variabili di tipo possono nascondere degli isomorfismi che non sono cos\`i evidenti ad una prima analisi, ad esempio i tipi:
\[
	\forall \alpha, \beta. \alpha \to \beta \to \alpha \ {\stackrel{?}{\cong}}\  \forall \gamma, \delta. \gamma \to \delta \to \delta  
\]
sembrerebbero non essere isomorfi in quanto i loro codomini non sono equivalenti. Se, come nel caso precedente, riscrivo $\alpha$ in $\gamma$ e $\beta$ in $\delta$ si ottengono:
\[
	\forall \alpha, \beta. \gamma \to \delta \to \gamma \not\cong \forall \gamma, \delta. \gamma \to \delta \to \delta  
\]
i quali potrebbero rappresentare i tipi di due funzioni che prendono in ingresso gli stessi valori ma restituiscono due risultati distinti. Chiaramente queste non risultano essere isomorfe, tuttavia un'ulteriore ridenominazione delle variabili potrebbe essere quella in cui $\alpha$ diventa $\delta$ e $\beta$ diventa $\gamma$ ottenendo:
\[
	\forall \alpha, \beta. \delta \to \gamma \to \delta \cong \forall \gamma, \delta. \gamma \to \delta \to \delta 
\]
che in base alla regola swap sono isomorfe.

Nell'implementazione pratica di questo passaggio, per evitare un ulteriore aumento combinatorio del numero di casi da verificare, verr\`a adottato un algoritmo di unificazione simile a quello utilizzato nei sistemi di type inference dei linguaggi funzionali.
Piuttosto che generare tutte le permutazioni delle variabili, rinominandole, verr\`a creato un ambiente definito di \textit{renaming} inizialmente vuoto, nel quale verranno memorizzate, in modo incrementale, le permutazioni che permettono di dimostrare che due variabili di tipo sono equivalenti. 
Nel verificare l'unificazione di due variabili si procede nel seguente modo:
\begin{itemize}
\item se una coppia di variabili $(\alpha_1, \alpha_2)$ \`e presente nell'ambiente di \textit{renaming}, allora \`e possibile affermare che queste sono equivalenti e non \`e necessario modificare in alcun modo l'ambiente.

\item Se una delle due variabili compare all'interno dell'ambiente di \textit{renaming} ma \`e in coppia con un'altra variabile l'algoritmo fallisce. Questo succede in quanto non si sta effettuando una vera e propria unificazione ma si stanno cercando delle permutazioni. Pertanto non \`e possibile che una stessa variabile sia associata con pi\`u variabili nell'altro tipo.

\item Se due variabili $(\alpha_1, \alpha_2)$ non compaiono nell'ambiente di \textit{renaming} significa che \`e stata individuata una nuova permutazione pertanto sar\`a necessario memorizzarla nell'ambiente di \textit{renaming}. Essendo la definizione di permutazione simmetrica verranno quindi aggiunte all'ambiente le coppie $(\alpha_1, \alpha_2)$ e $(\alpha_2, \alpha_1)$.
\end{itemize}

\subsubsection{Conclusioni}
In sintesi possiamo affermare che il confronto tra tipi viene effettuato in questo modo:
\begin{enumerate}
\item verifica dell'esistenza di una permutazione delle coppie del primo tipo che permetta di individuare un isomorfismo,
\item verifica dell'isomorfismo all'interno delle coordinate dei tipi,
\item verifica dell'esistenza di una unificazione delle variabili di tipo.
\end{enumerate}

Tutte le fasi, ad eccezione della terza, effettuano un confronto sulle permutazioni degli elementi di un tipo. Sapendo che il numero di permutazioni possibili su $n$ valori \`e $n!$ si ottiene che il numero complessivo di confronti \`e pari a:
\[
	n_{coordinate}! \times n_{argomenti}!
\]
si potrebbe quindi pensare che il numero di test su un tipo, generalmente molto complesso, faccia crescere troppo i tempi di calcolo.
\`E tuttavia importante ricordare che in tutte queste fasi viene effettuato un controllo preventivo sul numero di elementi, nel caso in cui questo valore sia diverso tra i tipi la risposta \`e pressoch\`e immediata. 

Per quanto riguarda la terza fase dell'algoritmo, come \`e stato precedentemente descritto, nell'implementazione pratica si utilizzer\`a una tecnica di unificazione che permetter\`a di rendere lineare il calcolo degli isomorfismi sulle variabili di tipo.
Inoltre, secondo un'indagine condotta da Rittri~\cite{Retriving_1992, Using_1989} il numero di variabili all'interno di un tipo mediamente complesso risulta essere generalmente inferiore a tre.



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "tesi"
%%% End: 	